Step of Proof: p-mu-exists 11,40

Inference at * 2 
Iof proof for Lemma p-mu-exists:



1. P : 
2. (n:. ((P(n))))
  x: + Top. p-mu(P;x
latex

 by (InstConcl [inr  ]) 
CollapseTHEN ((Auto
CollapseTHEN ((UnfoldTopAb 0) 
CollapseTHEN ((
CReduce 0) 
CollapseTHEN ((Auto
CollapseTHEN ((ParallelOp ( -2)
CollapseTHEN ((InstConcl [
Ci]) 
CollapseTHEN (Auto))))))) 
latex


C.


Definitionsinr x , , p-mu(P;x), , {x:AB(x)} , , A  B, Void, x:AB(x), A, P  Q, False, x:AB(x), b, x:AB(x), f(a), t  T
Lemmasassert wf

origin